ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), i:Id, es:event_system{i:l}.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (e1,e2,e:es-E(es).
 (loc(e2) = i)
  (loc(e1) = i)
  es-le(es; e; e2)
  iseg(event-info(ds;da); es-hist{i:l}(es;e1;e); es-hist{i:l}(es;e1;e2))) 

latex

Definitions

iseg(T; l1; l2), x:A. B(x), t  T, subtype(S; T), [e, e'], b, P  Q, False, A, es-info(es;e), event-info(ds;da), es-hist{i:l}(es;e1;e2), x. t(x), fpf(A; a.B(a)), Knd, event_system{i:l}, top, id-deq, fpf-cap(f; eq; x; z), es-vartype(es; i; x), es-kind(es; e), Kind-deq, es-valtype(es; e), prop{i:l}, es-le(es; e; e'), loc(e), Id, es-E(es), guard(T), sq_type(T), P  Q, decidable(P), trans(T; x,y.E(x;y)), P  Q, P  Q, P  Q, es-locl(es; e; e'), strong-subtype(A; B)

Lemmas

iseg-subtype, strong-subtype-set3, strong-subtype-self, nil iseg, decidable es-locl, es-le-not-locl, not wf, es-locl wf, not functionality wrt iff, es-locl-iff, es-interval-nil, iseg wf, es-le-trans, es-interval-iseg, decidable es-le, Id sq, es-le wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, Knd wf, fpf wf, iseg map, event-info wf, es-info wf, es-le-loc, es-loc-pred, es-interval wf, es-interval wf2, es-E wf, Id wf, es-loc wf